<!DOCTYPE html>
<html lang="zh-CN">
<head>
  <meta charset="UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1, maximum-scale=2">
<meta name="theme-color" content="#222">
<meta name="generator" content="Hexo 4.2.1">
  <link rel="icon" type="image/png" sizes="32x32" href="/images/32x32.png">
  <link rel="icon" type="image/png" sizes="16x16" href="/images/16x16.png">

<link rel="stylesheet" href="/css/main.css">

<link rel="stylesheet" href="//fonts.googleapis.com/css?family=Lato:300,300italic,400,400italic,700,700italic|Lato', 'Microsoft Yahei Light:300,300italic,400,400italic,700,700italic|Cambria', 'Microsoft Yahei Light:300,300italic,400,400italic,700,700italic|Verdana', Lato, 'Microsoft Yahei Light:300,300italic,400,400italic,700,700italic&display=swap&subset=latin,latin-ext">
<link rel="stylesheet" href="/lib/font-awesome/css/all.min.css">

<script id="hexo-configurations">
    var NexT = window.NexT || {};
    var CONFIG = {"hostname":"yoursite.com","root":"/","scheme":"Mist","version":"7.8.0","exturl":false,"sidebar":{"position":"right","display":"hide","padding":18,"offset":12,"onmobile":false},"copycode":{"enable":false,"show_result":false,"style":null},"back2top":{"enable":true,"sidebar":false,"scrollpercent":false},"bookmark":{"enable":false,"color":"#222","save":"auto"},"fancybox":false,"mediumzoom":false,"lazyload":false,"pangu":false,"comments":{"style":"tabs","active":null,"storage":true,"lazyload":false,"nav":null},"algolia":{"hits":{"per_page":10},"labels":{"input_placeholder":"Search for Posts","hits_empty":"We didn't find any results for the search: ${query}","hits_stats":"${hits} results found in ${time} ms"}},"localsearch":{"enable":true,"trigger":"auto","top_n_per_article":1,"unescape":false,"preload":false},"motion":{"enable":true,"async":false,"transition":{"post_block":"fadeIn","post_header":"slideDownIn","post_body":"slideDownIn","coll_header":"slideLeftIn","sidebar":"slideUpIn"}},"path":"search.xml"};
  </script>

  <meta name="description" content="Problem 623 Lambda CountThe lambda-calculus is a universal model of computation at the core of functional programming languages. It is based on lambda-terms, a minimal programming language featuring">
<meta property="og:type" content="article">
<meta property="og:title" content="Problem 623">
<meta property="og:url" content="http://yoursite.com/623/index.html">
<meta property="og:site_name" content="Project Euler | 欧拉计划">
<meta property="og:description" content="Problem 623 Lambda CountThe lambda-calculus is a universal model of computation at the core of functional programming languages. It is based on lambda-terms, a minimal programming language featuring">
<meta property="og:locale" content="zh_CN">
<meta property="article:published_time" content="2018-03-25T17:00:00.000Z">
<meta property="article:modified_time" content="2020-06-09T07:34:47.467Z">
<meta property="article:author" content="sx349">
<meta name="twitter:card" content="summary">

<link rel="canonical" href="http://yoursite.com/623/">


<script id="page-configurations">
  // https://hexo.io/docs/variables.html
  CONFIG.page = {
    sidebar: "",
    isHome : false,
    isPost : true,
    lang   : 'zh-CN'
  };
</script>

  <title>Problem 623 | Project Euler | 欧拉计划</title>
  






  <noscript>
  <style>
  .use-motion .brand,
  .use-motion .menu-item,
  .sidebar-inner,
  .use-motion .post-block,
  .use-motion .pagination,
  .use-motion .comments,
  .use-motion .post-header,
  .use-motion .post-body,
  .use-motion .collection-header { opacity: initial; }

  .use-motion .site-title,
  .use-motion .site-subtitle {
    opacity: initial;
    top: initial;
  }

  .use-motion .logo-line-before i { left: initial; }
  .use-motion .logo-line-after i { right: initial; }
  </style>
</noscript>

</head>

<body itemscope itemtype="http://schema.org/WebPage">
  <div class="container use-motion">
    <div class="headband"></div>

    <header class="header" itemscope itemtype="http://schema.org/WPHeader">
      <div class="header-inner"><div class="site-brand-container">
  <div class="site-nav-toggle">
    <div class="toggle" aria-label="切换导航栏">
      <span class="toggle-line toggle-line-first"></span>
      <span class="toggle-line toggle-line-middle"></span>
      <span class="toggle-line toggle-line-last"></span>
    </div>
  </div>

  <div class="site-meta">

    <a href="/" class="brand" rel="start">
      <span class="logo-line-before"><i></i></span>
      <h1 class="site-title">Project Euler | 欧拉计划</h1>
      <span class="logo-line-after"><i></i></span>
    </a>
  </div>

  <div class="site-nav-right">
    <div class="toggle popup-trigger">
        <i class="fa fa-search fa-fw fa-lg"></i>
    </div>
  </div>
</div>




<nav class="site-nav">
  <ul id="menu" class="main-menu menu">
        <li class="menu-item menu-item-home">

    <a href="/" rel="section"><i class="fa fa-home fa-fw"></i>首页</a>

  </li>
        <li class="menu-item menu-item-problem">

    <a href="/problems" rel="section"><i class="fa fa-tags fa-fw"></i>题目</a>

  </li>
        <li class="menu-item menu-item-about">

    <a href="/about/" rel="section"><i class="fa fa-user fa-fw"></i>关于</a>

  </li>
      <li class="menu-item menu-item-search">
        <a role="button" class="popup-trigger"><i class="fa fa-search fa-fw"></i>搜索
        </a>
      </li>
  </ul>
</nav>



  <div class="search-pop-overlay">
    <div class="popup search-popup">
        <div class="search-header">
  <span class="search-icon">
    <i class="fa fa-search"></i>
  </span>
  <div class="search-input-container">
    <input autocomplete="off" autocapitalize="off"
           placeholder="搜索..." spellcheck="false"
           type="search" class="search-input">
  </div>
  <span class="popup-btn-close">
    <i class="fa fa-times-circle"></i>
  </span>
</div>
<div id="search-result">
  <div id="no-result">
    <i class="fa fa-spinner fa-pulse fa-5x fa-fw"></i>
  </div>
</div>

    </div>
  </div>

</div>
    </header>

    
  <div class="back-to-top">
    <i class="fa fa-arrow-up"></i>
    <span>0%</span>
  </div>


    <main class="main">
      <div class="main-inner">
        <div class="content-wrap">
          

          <div class="content post posts-expand">
            

    
  
  
  <article itemscope itemtype="http://schema.org/Article" class="post-block" lang="zh-CN">
    <link itemprop="mainEntityOfPage" href="http://yoursite.com/623/">

    <span hidden itemprop="author" itemscope itemtype="http://schema.org/Person">
      <meta itemprop="image" content="/images/avatar.png">
      <meta itemprop="name" content="sx349">
      <meta itemprop="description" content="Project Euler | 欧拉计划 中文翻译站">
    </span>

    <span hidden itemprop="publisher" itemscope itemtype="http://schema.org/Organization">
      <meta itemprop="name" content="Project Euler | 欧拉计划">
    </span>
      <header class="post-header">
        <h1 class="post-title" itemprop="name headline">
          Problem 623
        </h1>

        <div class="post-meta">
            <span class="post-meta-item">
              <span class="post-meta-item-icon">
                <i class="far fa-calendar"></i>
              </span>
              <span class="post-meta-item-text">题目发布于</span>

              <time title="发布时间：2018-03-25 10:00:00" itemprop="dateCreated datePublished" datetime="2018-03-25T10:00:00-07:00">2018-03-25</time>
            </span>
              <span class="post-meta-item">
                <span class="post-meta-item-icon">
                  <i class="far fa-calendar-check"></i>
                </span>
                <span class="post-meta-item-text">翻译更新于</span>
                <time title="更新时间：2020-06-09 00:34:47" itemprop="dateModified" datetime="2020-06-09T00:34:47-07:00">2020-06-09</time>
              </span>

          

        </div>
      </header>

    
    
    
    <div class="post-body" itemprop="articleBody">

      
        <hr>
<h1 id="Problem-623"><a href="#Problem-623" class="headerlink" title="Problem 623"></a><a href="https://projecteuler.net/problem=623" target="_blank" rel="noopener">Problem 623</a></h1><hr>
<h2 id="Lambda-Count"><a href="#Lambda-Count" class="headerlink" title="Lambda Count"></a><strong>Lambda Count</strong></h2><p>The <i>lambda-calculus</i> is a universal model of computation at the core of functional programming languages. It is based on <i>lambda-terms</i>, a minimal programming language featuring only function definitions, function calls and variables. Lambda-terms are built according to the following rules:</p>
<ul>
<li>Any variable $x$ (single letter, from some infinite alphabet) is a lambda-term.</li>
<li>If $M$ and $N$ are lambda-terms, then $(MN)$ is a lambda-term, called the <i>application</i> of $M$ to $N$.</li>
<li>If $x$ is a variable and $M$ is a term, then $(\lambda x.M)$ is a lambda-term, called an <i>abstraction</i>. An abstraction defines an anonymous function, taking $x$ as parameter and sending back $M$.</li>
</ul>
<p>A lambda-term $T$ is said to be <i>closed</i> if for all variables $x$, all occurrences of $x$ within $T$ are contained within some abstraction $(\lambda x.M)$ in $T$. The smallest such abstraction is said to <i>bind</i> the occurrence of the variable $x$. In other words, a lambda-term is closed if all its variables are bound to parameters of enclosing functions definitions. For example, the term $(\lambda x.x)$ is closed, while the term $(\lambda x.(xy))$ is not because $y$ is not bound.</p>
<p>Also, we can rename variables as long as no binding abstraction changes. This means that $(\lambda x.x)$ and $(\lambda y.y)$ should be considered equivalent since we merely renamed a parameter. Two terms equivalent modulo such renaming are called <i>$\alpha$-equivalent</i>. Note that $(\lambda x.(\lambda y.(xy)))$ and $(\lambda x.(\lambda x.(xx)))$ are not $\alpha$-equivalent, since the abstraction binding the first variable was the outer one and becomes the inner one. However, $(\lambda x.(\lambda y.(xy)))$ and $(\lambda y.(\lambda x.(yx)))$ are $\alpha$-equivalent.</p>
<p>The following table regroups the lambda-terms that can be written with at most $15$ symbols, symbols being parenthesis, $\lambda$, dot and variables.</p>
<table>
<thead>
<tr>
<th></th>
<th></th>
<th></th>
<th></th>
</tr>
</thead>
<tbody><tr>
<td>$(\lambda x.x)$</td>
<td>$(\lambda x.(x(xx)))$</td>
<td>$(\lambda x.(\lambda y.(yx)))$</td>
<td>$(\lambda x.((\lambda y.x)x))$</td>
</tr>
<tr>
<td>$(\lambda x.(x((xx)x)))$</td>
<td>$(\lambda x.(xx))$</td>
<td>$(\lambda x.((xx)x))$</td>
<td>$(\lambda x.(\lambda y.(yy)))$</td>
</tr>
<tr>
<td>$(\lambda x.((\lambda y.y)x))$</td>
<td>$(\lambda x.((xx)(xx)))$</td>
<td>$(\lambda x.(\lambda y.x))$</td>
<td>$(\lambda x.(\lambda y.(xx)))$</td>
</tr>
<tr>
<td>$(\lambda x.(x(\lambda y.x)))$</td>
<td>$((\lambda x.x)(\lambda x.x))$</td>
<td>$(\lambda x.((x(xx))x))$</td>
<td>$(\lambda x.(\lambda y.y))$</td>
</tr>
<tr>
<td>$(\lambda x.(\lambda y.(xy)))$</td>
<td>$(\lambda x.(x(\lambda y.y)))$</td>
<td>$(\lambda x.(x(x(xx))))$</td>
<td>$(\lambda x.(((xx)x)x))$</td>
</tr>
</tbody></table>
<p>Let $\Lambda(n)$ be the number of distinct closed lambda-terms that can be written using at most $n$ symbols, where terms that are $\alpha$-equivalent to one another should be counted only once. You are given that $\Lambda(6)=1$, $\Lambda(9)=2$, $\Lambda(15)=20$ and $\Lambda(35)=3166438$.</p>
<p>Find $\Lambda(2000)$. Give the answer modulo $1000000007$.</p>
<hr>
<h2 id="lambda计数"><a href="#lambda计数" class="headerlink" title="lambda计数"></a><strong>lambda计数</strong></h2><p><i class=zh>lambda演算</i>是作为函数式编程语言核心的一种通用计算模型。这种模型基于<i class=zh>lambda项</i>，这是一种只包含函数定义、函数调用和变量的极简编程语言。lambda项根据如下的规则进行构建：</p>
<ul>
<li>任意变量$x$（由单个字母表示，假定字母表的长度无穷）都是lambda项。</li>
<li>如果$M$和$N$是lambda项，那么$(MN)$也是lambda项，这被称为将$M$<i class=zh>应用</i>到$N$上。</li>
<li>如果$x$是一个变量而$M$是一个lambda项，那么$(\lambda x.M)$是一个lambda项，这被称为<i class=zh>抽象</i>。 一个抽象定义了一个匿名函数，其中$x$是参数并返回$M$。</li>
</ul>
<p>如果在一个lambda项$T$中出现过的所有变量$x$均包含于$T$中的某个抽象$(\lambda x.M)$，则称$T$为<i class=zh>闭合</i>的，并称包含$x$的抽象中最小的一个<i class=zh>绑定</i>了$x$。换言之，如果一个lambda项中出现的所有变量都被绑定为某个函数定义中的参数，则它是闭合的。例如，lambda项$(\lambda x.x)$是闭合的，而lambda项$(\lambda x.(xy))$则不是，因为$y$并未被绑定。</p>
<p>另外，只要不改变抽象的绑定关系，我们可以随意重命名变量。这意味着$(\lambda x.x)$和$(\lambda y.y)$应当被认为是等价的，因为我们只是重命名了一个参数。在这样的重命名中等价的两个lambda项被称为<i class=zh>$\alpha$-等价</i>。注意$(\lambda x.(\lambda y.(xy)))$和$(\lambda x.(\lambda x.(xx)))$并不是$\alpha$-等价的，因为前者中绑定第一个变量的抽象是外层的抽象，而后者中则变成了内层的抽象。不过，$(\lambda x.(\lambda y.(xy)))$和$(\lambda y.(\lambda x.(yx)))$是$\alpha$-等价的。</p>
<p>如下的表格展示了所有可以用至多$15$个符号表示的lambda项，这里的符号包括括号，$\lambda$，点号和变量名。</p>
<table>
<thead>
<tr>
<th></th>
<th></th>
<th></th>
<th></th>
</tr>
</thead>
<tbody><tr>
<td>$(\lambda x.x)$</td>
<td>$(\lambda x.(x(xx)))$</td>
<td>$(\lambda x.(\lambda y.(yx)))$</td>
<td>$(\lambda x.((\lambda y.x)x))$</td>
</tr>
<tr>
<td>$(\lambda x.(x((xx)x)))$</td>
<td>$(\lambda x.(xx))$</td>
<td>$(\lambda x.((xx)x))$</td>
<td>$(\lambda x.(\lambda y.(yy)))$</td>
</tr>
<tr>
<td>$(\lambda x.((\lambda y.y)x))$</td>
<td>$(\lambda x.((xx)(xx)))$</td>
<td>$(\lambda x.(\lambda y.x))$</td>
<td>$(\lambda x.(\lambda y.(xx)))$</td>
</tr>
<tr>
<td>$(\lambda x.(x(\lambda y.x)))$</td>
<td>$((\lambda x.x)(\lambda x.x))$</td>
<td>$(\lambda x.((x(xx))x))$</td>
<td>$(\lambda x.(\lambda y.y))$</td>
</tr>
<tr>
<td>$(\lambda x.(\lambda y.(xy)))$</td>
<td>$(\lambda x.(x(\lambda y.y)))$</td>
<td>$(\lambda x.(x(x(xx))))$</td>
<td>$(\lambda x.(((xx)x)x))$</td>
</tr>
</tbody></table>
<p>记$\Lambda(n)$为可以用至多$n$个符号表示的不同闭合lambda项的数目，其中$\alpha$-等价的lambda项只计算一次。已知$\Lambda(6)=1$，$\Lambda(9)=2$，$\Lambda(15)=20$以及$\Lambda(35)=3166438$。</p>
<p>求$\Lambda(2000)$，并将答案对$1000000007$取模。</p>
<hr>

    </div>

    
    
    

      <footer class="post-footer">

        


        
    <div class="post-nav">
      <div class="post-nav-item">
    <a href="/622/" rel="prev" title="Problem 622">
      <i class="fa fa-chevron-left"></i> Problem 622
    </a></div>
      <div class="post-nav-item">
    <a href="/624/" rel="next" title="Problem 624">
      Problem 624 <i class="fa fa-chevron-right"></i>
    </a></div>
    </div>
      </footer>
    
  </article>
  
  
  



          </div>
          
    <div class="comments" id="gitalk-container"></div>

<script>
  window.addEventListener('tabs:register', () => {
    let { activeClass } = CONFIG.comments;
    if (CONFIG.comments.storage) {
      activeClass = localStorage.getItem('comments_active') || activeClass;
    }
    if (activeClass) {
      let activeTab = document.querySelector(`a[href="#comment-${activeClass}"]`);
      if (activeTab) {
        activeTab.click();
      }
    }
  });
  if (CONFIG.comments.storage) {
    window.addEventListener('tabs:click', event => {
      if (!event.target.matches('.tabs-comment .tab-content .tab-pane')) return;
      let commentClass = event.target.classList[1];
      localStorage.setItem('comments_active', commentClass);
    });
  }
</script>

        </div>
          
  
  <div class="toggle sidebar-toggle">
    <span class="toggle-line toggle-line-first"></span>
    <span class="toggle-line toggle-line-middle"></span>
    <span class="toggle-line toggle-line-last"></span>
  </div>

  <aside class="sidebar">
    <div class="sidebar-inner">

      <ul class="sidebar-nav motion-element">
        <li class="sidebar-nav-toc">
          文章目录
        </li>
        <li class="sidebar-nav-overview">
          站点概览
        </li>
      </ul>

      <!--noindex-->
      <div class="post-toc-wrap sidebar-panel">
          <div class="post-toc motion-element"><ol class="nav"><li class="nav-item nav-level-1"><a class="nav-link" href="#Problem-623"><span class="nav-text">Problem 623</span></a><ol class="nav-child"><li class="nav-item nav-level-2"><a class="nav-link" href="#Lambda-Count"><span class="nav-text">Lambda Count</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#lambda计数"><span class="nav-text">lambda计数</span></a></li></ol></li></ol></div>
      </div>
      <!--/noindex-->

      <div class="site-overview-wrap sidebar-panel">
        <div class="site-author motion-element" itemprop="author" itemscope itemtype="http://schema.org/Person">
    <img class="site-author-image" itemprop="image" alt="sx349"
      src="/images/avatar.png">
  <p class="site-author-name" itemprop="name">Leonhard Euler(1707-1783)</p>
  <p class="site-description motion-element">Project Euler | 欧拉计划<br>中文翻译站</p>
</div>
  <div class="cc-license motion-element" itemprop="license">
    <a href="https://creativecommons.org/licenses/by-nc-sa/4.0/" class="cc-opacity" rel="noopener" target="_blank"><img src="/images/cc-by-nc-sa.svg" alt="Creative Commons"></a>
  </div>


  <div class="links-of-blogroll motion-element">
    <div class="links-of-blogroll-title"><i class="fa fa-link fa-fw"></i>
      友情链接
    </div>
    <ul class="links-of-blogroll-list">
        <li class="links-of-blogroll-title">
          <a href="https://projecteuler.net/" title="https:&#x2F;&#x2F;projecteuler.net" rel="noopener" target="_blank">Project Euler</a>
        </li>
        <li class="links-of-blogroll-title">
          <a href="http://jakwings.is-programmer.com/Project_Euler" title="http:&#x2F;&#x2F;jakwings.is-programmer.com&#x2F;Project_Euler" rel="noopener" target="_blank">饮水思源汉化</a>
        </li>
        <li class="links-of-blogroll-title">
          <a href="http://sx349.github.io/" title="http:&#x2F;&#x2F;sx349.github.io" rel="noopener" target="_blank">译者博客</a>
        </li>
    </ul>
  </div>

      </div>

    </div>
  </aside>
  <div id="sidebar-dimmer"></div>


      </div>
    </main>

    <footer class="footer">
      <div class="footer-inner">
        

        

<div class="copyright">
  
  &copy; 2001 – 
  <span itemprop="copyrightYear">2021</span>
  <span class="with-love">
    <i class="fas fa-calculator"></i>
  </span>
  <span class="author" itemprop="copyrightHolder">Project Euler | 欧拉计划</span>
</div>
  <div class="powered-by">由 <a href="https://hexo.io/" class="theme-link" rel="noopener" target="_blank">Hexo</a> & <a href="https://mist.theme-next.org/" class="theme-link" rel="noopener" target="_blank">NexT.Mist</a> 强力驱动
  </div>

        








      </div>
    </footer>
  </div>

  
  <script src="/lib/anime.min.js"></script>
  <script src="/lib/velocity/velocity.min.js"></script>
  <script src="/lib/velocity/velocity.ui.min.js"></script>

<script src="/js/utils.js"></script>

<script src="/js/motion.js"></script>


<script src="/js/schemes/muse.js"></script>


<script src="/js/next-boot.js"></script>




  




  
<script src="/js/local-search.js"></script>













  

  
      

<script>
  if (typeof MathJax === 'undefined') {
    window.MathJax = {
      loader: {
        source: {
          '[tex]/amsCd': '[tex]/amscd',
          '[tex]/AMScd': '[tex]/amscd'
        }
      },
      tex: {
        inlineMath: {'[+]': [['$', '$']]},
        tags: 'ams'
      },
      options: {
        renderActions: {
          findScript: [10, doc => {
            document.querySelectorAll('script[type^="math/tex"]').forEach(node => {
              const display = !!node.type.match(/; *mode=display/);
              const math = new doc.options.MathItem(node.textContent, doc.inputJax[0], display);
              const text = document.createTextNode('');
              node.parentNode.replaceChild(text, node);
              math.start = {node: text, delim: '', n: 0};
              math.end = {node: text, delim: '', n: 0};
              doc.math.push(math);
            });
          }, '', false],
          insertedScript: [200, () => {
            document.querySelectorAll('mjx-container').forEach(node => {
              let target = node.parentNode;
              if (target.nodeName.toLowerCase() === 'li') {
                target.parentNode.classList.add('has-jax');
              }
            });
          }, '', false]
        }
      }
    };
    (function () {
      var script = document.createElement('script');
      script.src = '//cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js';
      script.defer = true;
      document.head.appendChild(script);
    })();
  } else {
    MathJax.startup.document.state(0);
    MathJax.texReset();
    MathJax.typeset();
  }
</script>

    

  

<link rel="stylesheet" href="//cdn.jsdelivr.net/npm/gitalk@1/dist/gitalk.min.css">

<script>
NexT.utils.loadComments(document.querySelector('#gitalk-container'), () => {
  NexT.utils.getScript('//cdn.jsdelivr.net/npm/gitalk@1/dist/gitalk.min.js', () => {
    var gitalk = new Gitalk({
	  title       : document.title.substr(0,29),
      clientID    : '4ba99a8839c5e7dde683',
      clientSecret: '3984f7cad409553d6afde8dbc2c08fc425e7bbdc',
      repo        : 'pe-cn-comments',
      owner       : 'pe-cn',
      admin       : ['sx349'],
      id          : '4969b7d641ed6ad8d08d43ac87e7969e',
        language: '',
      distractionFreeMode: true
    });
    gitalk.render('gitalk-container');
  }, window.Gitalk);
});
</script>

</body>
</html>
